@catcodes
boldOT1cmssbxn
boldOT1cmrbxit
` ="8000 `=́"8000 `_="8000 (operators"28largesymbols"00
)operators"29largesymbols"01
[operators"5Blargesymbols"02
]operators"5Dlargesymbols"03
/operators"2Flargesymbols"0E
<symbols"68largesymbols"0A
>symbols"69largesymbols"0B
|symbols"6Alargesymbols"0C
backslashchar
symbols"6Elargesymbols"0F
¬=¬#neg;
&and#land;=&and#wedge;
&or#lor;=&or#vee;
&ne#ne;==
&le#le;=&le#leq;
&ge#ge;=&ge#geq;
&ni#owns;=&ni#ni;
&larr#gets;=&larr#leftarrow;
&rarr#to;=&rarr#rightarrow;
´operators"13
`operators"12
¨operators"7F
˜operators"7E
¯operators"16
˘operators"15
ˇoperators"14
ˆoperators"5E
letters"7E
˙operators"5F
largesymbols"65
largesymbols"62
symbols"70largesymbols"70
largesymbols"7Alargesymbols"40
largesymbols"7Blargesymbols"41
symbols"6Alargesymbols"3C
symbols"6Blargesymbols"3D
||
symbols"6Blargesymbols"0D
||=||
&vert#vert;
symbols"6Alargesymbols"0C
&uarr#uparrow;
symbols"22largesymbols"78
&darr#downarrow;
symbols"23largesymbols"79
&varr#updownarrow;
symbols"6Clargesymbols"3F
&uArr#Uparrow;
symbols"2Alargesymbols"7E
&dArr#Downarrow;
symbols"2Blargesymbols"7F
&vArr#Updownarrow;
symbols"6Dlargesymbols"77
#1363#> symbols"6Elargesymbols"0F
&rang#rangle;
symbols"69largesymbols"0B
&lang#langle;
symbols"68largesymbols"0A
}
symbols"67largesymbols"09
{
symbols"66largesymbols"08
&rceil#rceil;
symbols"65largesymbols"07
&lceil#lceil;
symbols"64largesymbols"06
&rfloor#rfloor;
symbols"63largesymbols"05
&lfloor#lfloor;
symbols"62largesymbols"04
largesymbols"3Alargesymbols"3A
largesymbols"3Blargesymbols"3B
largesymbols"3Elargesymbols"3E
=3mu
=4mu plus 2mu minus 4mu
=5mu plus 5mu